es:event_system{i:l}, e,e',ev:es-E(es).
(ev  [e, e'])  (es-le(es; e; ev)  es-le(es; ev; e')) 

latex

Definitions	x:A. B(x), t  T, P  Q, [e, e'], P  Q, P  Q, prop{i:l}, P  Q, P  Q, es-le(es; e; e'), guard(T), False
Lemmas	es-E wf, event system wf, iff functionality wrt iff, l member wf, filter wf, es-ble wf, append wf, es-before wf, assert wf, es-le wf, member filter, and functionality wrt iff, member append, es-locl wf, or functionality wrt iff, member-es-before, cons member, false wf, nil member, assert-es-ble